$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$a$, $b$:$T$. Dec($a$ = $b$))
\\[0ex]$\Rightarrow$ ($\forall$$a$, $b$:$T$. Dec($R$($a$,$b$)))
\\[0ex]$\Rightarrow$ Linorder($T$;$a$,$b$.$R$($a$,$b$))
\\[0ex]$\Rightarrow$ ($\forall$$L$:($T$ List). $\exists$${\it L'}$:$T$ List. (sorted{-}by($R$;${\it L'}$) \& no\_repeats($T$;${\it L'}$) \& $L$ $\subseteq$ ${\it L'}$ \& ${\it L'}$ $\subseteq$ $L$))